nLab Lawvere theory

Redirected from "Lawvere theories".
Contents

Context

Categorical algebra

Higher algebra

Contents

Idea

The notion of Lawvere theory is a joint generalization of the notions of group, ring, associative algebra, etc.

In his 1963 doctoral dissertation, Bill Lawvere introduced a new categorical method for doing universal algebra, alternative to the usual way of presenting an algebraic concept by means of its logical signature (with generating operations satisfying equational axioms). The rough idea is to define an algebraic theory as a category with finite products and possessing a “generic algebra” (e.g., a generic group), and then define a model of that theory (e.g., a group) as a product-preserving functor out of that category. This type of category is what is nowadays called a Lawvere algebraic theory, or just Lawvere theory.

Definition

There are two related definitions of Lawvere theory in the literature. Both definitions are widely used and both have a substantial history.

Definition A

A Lawvere theory or finite-product theory is (equivalently encoded by its syntactic category which is) a category TT with finite products in which every object is isomorphic to a finite cartesian power x n=x×x××xx^n = x \times x \times \cdots \times x of a distinguished object xx (called the generic object for the theory TT).

A homomorphism of such theories TTT \to T' is a product-preserving functor which also preserves the generic object.

Definition B

Let 𝔽\mathbb{F} be the category of natural numbers and functions between them (a skeleton of the category of finite sets). This category has canonical chosen coproducts.

A Lawvere theory is a category TT equipped with an identity-on-objects strictly power-preserving functor J:𝔽 opTJ:\mathbb{F}^{\mathrm{op}} \to T. (Power preservation is here equivalent to product preservation.)

In this definition, a homomorphism is a product-preserving functor making the obvious triangle commute strictly.

Remark

Clearly, if TT is part of a structure in the form of Definition B, then TT is of the form in Definition A, taking x=J(1)x=J(1). See further remarks below.

For TT a Lawvere theory, we are to think of the hom-set T(n,1):=T(x n,x)T(n,1) := T(x^n, x) as the set of nn-ary operations definable in the theory. For instance for TT the theory of abelian groups, T(2,1)T(2,1) includes operations like +:(x,y)x+y+ \colon (x, y) \mapsto x + y, :(x,y)xy- \colon (x, y) \mapsto x-y, and (x,y)2x3y(x, y) \mapsto 2 x - 3 y. For 00-ary or nullary operations, we have T(0,1)={0}T(0,1) = \{0\}.

Definition

A model of TT – an algebra over the Lawvere theory or simply TT-algebra – is a product-preserving functor

A:TSet, A : T \to Set \,,

and homomorphism of TT-algebras is a natural transformation between such functors.

Remark

Such a functor picks out a single set U(A):=A(1)U(A) := A(1) and picks for every nn-ary abstract operation ϕT(n,1)\phi \in T(n,1) an actual nn-ary operation on the elements of this set

A(ϕ):U(A) nU(A) A(\phi) : U(A)^n \to U(A)

such that these operations are all compatible with each other in the way governed by the composition rules of morphisms in TT.

When working with Definition B of Lawvere theory, it would be normal to require that AA strictly preserves products.

Remarks

  1. From some perspectives, Definition B violates the principle of equivalence, although from another perspective it should be regarded as a basic structural definition that is equivalent in content to an abstract clone, or equivalently a relative monad over 𝔽\mathbb{F}. On the other hand, given a structure of the form Definition A, we may choose a power of xx for each natural number, and thus derive an essentially surjective product-preserving functor 𝔽 opT\mathbb{F}^{op} \to T, and then we can always factor this as an identity-on-objects functor to reach Definition B.

  2. Some people use ‘finite-product theory’ to mean any (small) category with finite products, reserving ‘Lawvere theory’ to refer to finite product theories with the property that every object is isomorphic to a product of finitely many copies of a given object xx. Finite-product theories CC can be regarded as a special case of multisorted Lawvere theories (see below) where the set of sorts is Ob(C)Ob(C) itself. Some, but not all, the above discussion generalizes to this case.

  3. As finite-product theories, Lawvere theories are at one end of a spectrum of theories of differing logical strengths. For example, there are left exact theories, regular theories, geometric theories, and so on, which require for their interpretation categories of differing degrees of strength in their internal logic. See also classifying topos.

  4. If CC is a category with finite products, then a group (object) in CC may be defined as a product-preserving functor T GrpCT_{Grp} \to C. For example, a topological group may be identified with a functor T GrpTopT_{Grp} \to Top, and a Lie group with a product-preserving functor T GrpManT_{Grp} \to Man into the category of smooth manifolds. An analogous statement holds for any finitary algebraic theory, when formulated in terms of its Lawvere theory TT.

Variations

  • A multisorted or multityped Lawvere theory for a given set of sorts SS is a category with finite products CC together with a function i:SOb(C)i: S \to Ob(C) such that every object of CC is isomorphic to a finite product of objects of the form i(S)i(S). An example is the theory for ring-module pairs, which may be regarded as a two-sorted theory in which one sort is interpreted as a ring and the other as a module over that ring.

  • An infinitary Lawvere theory allows for infinitary operations. An example is the theory of suplattices, where we have, for every cardinal number nn, an operation to take the supremum of nn elements. While Lawvere theories correspond to finitary monads on SetSet, infinitary Lawvere theories correspond to arbitrary monads.

  • A Fermat theory is a Lawvere theory equipped with a notion of differentiation.

  • A finite-product theory can also be presented without including all the products of the basic types as actual objects. This yields the notion of cartesian multicategory.

Examples

The theory of sets

The tautological example of a Lawvere theory is the algebraic theory of no operations. This is also called the theory of equality.

Its syntactic category is the category 𝒮\mathcal{S} on objects nn \in \mathbb{N} with morphisms generated by the projections π i:n1\pi_i : n \to 1. This is the opposite category of the category FinSet

𝒮FinSet op. \mathcal{S} \simeq FinSet^{op} \,.

This is the initial object in the category of Lawvere theories.

An algebra over this theory is just a bare set:

𝒮AlgSet. \mathcal{S} Alg \simeq Set \,.

For TT any Lawvere theory, there is a canonical morphism 𝒮T\mathcal{S} \to T. On categories of algebras this induces the functor

U T:TAlg𝒮AlgSet. U_T : T Alg \to \mathcal{S}Alg \simeq Set \,.

This sends each algebra to its underlying set . For more on this see the section Free T-algebras below.

The theory of groups

We consider here the theory of groups (defined however you like). To get the corresponding Lawvere theory TT, let F(n)F(n) (for any natural number n0n \geq 0) be a free group on nn generators, and define the Lawvere theory T GrpT_{Grp} to be the category opposite to the category of free groups F(n)F(n) and group homomorphisms. The generic object xx of T GrpT_{Grp} is taken to be F(1)F(1).

The category of free groups has finite coproducts since F(m)+F(n)F(m+n)F(m) + F(n) \cong F(m+n) (in other words, the inclusion

FreeGroupGroupFreeGroup \hookrightarrow Group

creates coproducts in FreeGroupFreeGroup), so T GrpT_{Grp} has finite products, and we have F(n)=x nF(n) = x^n in T GrpT_{Grp}. Any group GG defines a product-preserving functor

T Grp=FreeGroup opGroup ophom(,G)SetT_{Grp} = FreeGroup^{op} \hookrightarrow Group^{op} \stackrel{\hom(-, G)}{\to} Set

since contravariant hom-functors take coproducts to products. Thus any group gives a model of T GrpT_{Grp}.

The other direction is more interesting. Let

M:T GrpSetM: T_{Grp} \to Set

be a model of T GrpT_{Grp}, i.e., a product-preserving functor. We will define a group structure on G=M(x)G = M(x), the underlying set of the group.

To understand this, let’s consider how group multiplication would be defined. The idea is that xx in T GrpT_{Grp} is a “generic group”, so we first need to understand how multiplication works there. The idea is that the product in the generic group

m:x 2x 1m: x^2 \to x^1

corresponds to a homomorphism

F(1)F(2)F(1) \to F(2)

which by freeness corresponds to an element 1F(2)1 \to F(2), and the element we are after should be the product aba b of the generators a,ba, b of the free group F(2)=F(a,b)F(2) = F(a, b). The generators a,ba, b themselves correspond to the two coproduct inclusions

i 1:F(1)F(1)+F(1)=F(2)i 2:F(1)F(1)+F(1)=F(2)i_1: F(1) \to F(1) + F(1) = F(2) \qquad i_2: F(1) \to F(1) + F(1) = F(2)

Then, since MM is assumed to preserve products, we obtain a map

G×G=M(x)×M(x)M(x 2)M(m)M(x)=GG \times G = M(x) \times M(x) \cong M(x^2) \stackrel{M(m)}{\to} M(x) = G

and this defines the group multiplication on GG. The group identity and group inversion on GG are defined by following similar recipes.

It may be checked that the notion of homomorphism of T GrpT_{Grp}-models (as defined above) coincides with the usual notion of group homomorphism. In summary, the category of groups is equivalent to the category of models of T GrpT_{Grp}.

In particular, any hom-functor

hom T Grp(x n,):T GrpSet\hom_{T_{Grp}}(x^n, -): T_{Grp} \to Set

preserves products, and so defines a group. This group is precisely the free group on nn generators, and a little thought shows that the nn generators correspond to the natural transformations

hom T Grp(x,)hom T Grp(x n,)\hom_{T_{Grp}}(x, -) \to \hom_{T_{Grp}}(x^n, -)

induced by the nn projection maps x nxx^n \to x.

All of the discussion above for the case of groups generalizes to any finitary algebraic theory (i.e., any single-sorted theory whose signature consists of function symbols of finite arity, subject to universally quantified equational axioms). In summary:

  • The Lawvere theory TT is the category opposite to the category of free algebras on finitely many generators,

  • The category of algebras is in turn equivalent to the category of product-preserving functors TSetT \to Set, and

  • The free algebras are retrieved as the representable functors TSetT \to Set.

As discussed in the article on operads, the notion of Lawvere theory may also be formulated in terms of operads relative to the theory of cartesian monoidal categories.

Other examples

Most of the standard structures that are considered in algebra indeed are models of algebraic/Lawvere theories in the precise sense. The following list gives a few familiar examples and a few not so familiar ones, but there are many more. Beware though that there are also some familiar examples that seem to be algebraic but are not, these we discuss below.

Characterization of examples

If TT is any theory given by a signature consisting of finitary operations (but no relations) on a single sort, and a set of axioms all of which are universally quantified equations between terms, then a model of TT can be described as an algebra of a Lawvere theory.

This includes most cases arising in a typical undergraduate course in modern algebra, as the examples above suggest.

There are also well-known criteria for a category of single-sorted structures CC, with underlying set-functor U:CSetU: C \to Set, to be the category of algebras of a Lawvere theory.

Theorem

A concrete category U:CSetU \colon C \to Set is a category of algebras over a Lawvere theory precisely if UU

  1. is monadic

  2. is finitary in that it preserves filtered colimits.

Another characterization is:

Theorem

(Birkhoff's HSP theorem)

Suppose given a language LL generated by a set of (single-sorted) finitary operations, and a class CC of structures for LL. Then CC is the class of models for a set of universally quantified equations between terms of LL if and only if

  1. (H) The class is closed under homomorphic images,

  2. (S) The class is closed under subalgebras,

  3. (P) The class is closed under taking products.

Some non-examples

Here are some notable examples of mathematical structures that look algebraic, but are not models of an algebraic theory in the present sense:

  • The class of fields is not the class of algebras of a Lawvere theory.

  • Neither is the class of integral domains.

This might seem obvious since multiplicative inversion in fields is not a global operation, or otherwise the cancellation law of multiplication in integral domains is not a universally quantified axiom (since we have to make an exception of 00). But one should be careful that there isn’t some sneaky alternative axiomatization for these structures which counters these objections!

The first clause in Theorem already rules out fields, since UU in that case will create limits in CC, but the category Field of fields does not even have products. Similarly for integral domains.

The second clause in Theorem suggests another type of non-example:

  • The category SLatSLat of sup-lattices is not the category of algebras of a (finitary) Lawvere theory.

There is a whole class of infinitary sup-operations for sup-lattices (one for every arity = cardinal), but again one may wonder how one rules out any alternative finitary axiomatizations. But this is fairly clear by invoking the second clause and considering the following example: if U:SLatSetU: SLat \to Set created filtered colimits, then the countable copower 2\mathbb{N} \cdot \mathbf{2} of 2-element sup-lattices (which turns out to be the power set P()P(\mathbb{N}) with its usual order) would be the filtered colimit (in fact a union) over finite subsets SS of finite copowers S2S \cdot \mathbf{2}, hence a countable union of finite sup-lattices, which is clearly impossible.

Properties

Coequalizers of TT-algebras

Definition (congruence)

Let TT be a Lawvere theory and AA a TT-algebra. A congruence on AA is an equivalence relation on the set A(1)A(1) such that whenever for all nn \in \mathbb{N} whenever any (a iA(1)) i=1 n(a_i \in A(1))_{i=1}^n and (b iA(1)) i=1 n(b_i \in A(1))_{i=1}^n are pairwise equivalent, a ib ia_i \sim b_i, then also for every operation fT(n,1)f \in T(n,1) the results are equivalent: f(a 1,,a n)f(b 1,,b n)f(a_1, \cdot, a_n) \sim f(b_1, \cdots , b_n).

Observation/Definition

For AA a TT-algebra and for every relation RA(1)×A(1)R \subset A(1) \times A(1) there is a smallest congruence on AA containing RR. Write RA(1)×A(1)\langle R \rangle \subset A(1) \times A(1) for this smallest congruence.

Proposition

For AA a TT-algebra and CC a congruence on AA, the relation A/C(f)(A/C) n×A/CA/C(f) \subset (A/C)^n \times A/C induced by A(f)A(f) for each f:T(n,1)f : \in T(n,1) are functions and define a TT-algebra structure on A(1)/CA(1)/C.

Proposition

For f,g:ABf,g : A \to B two morphisms of TT-algebras, the canonical morphism BB/f(a)g(a)|aA(1)B \to B/\langle \f(a)\sim g(a) | a \in A(1)\rangle is the coequalizer of ff and gg.

Free TT-algebras and underlying sets

Write 𝒮\mathcal{S} for the (syntactic category of the) algebraic theory of sets (described above). Then for TT any other (syntactic category of a) Lawvere theory, there is a canonical morphism

i T:𝒮T. i_T : \mathcal{S} \to T \,.

By precomposition with i Ti_T we obtain a corresponding functor on TT-algebras, which we write

U T:TAlgSet U_T : T Alg \to Set

and call the underlying set functor.

Lemma

The functor U TU_T has a left adjoint F T:SetTAlgF_T : Set \to T Alg.

This is a standard example of a free functor, called the free TT-algebra functor.

Proof

For SS \in Set, let F T(S)F_T(S) be the TT-algebra whose underlying set is the set of formal expressions {f(s 1,,s n)|fT(n,1),s iS}\{f(s_1, \cdots, s_n) | f \in T(n,1), s_i \in S\} with the evident composition operation.

Observation

For S=(n)S = (n) \in FinSet a finite set with nn elements , the free TT-algebra on SS is just the representable

F T(S)=T(n,):TSet. F_T(S) = T(n,-) : T \to Set \,.

The adjunction isomorphism

TAlg(F T(S),A)Set(S,U T(A))(A(1)) nA(n) T Alg(F_T(S), A) \simeq Set(S, U_T(A)) \simeq (A(1))^n \simeq A(n)

is in this case just the Yoneda lemma.

TAlg(T(n,),A)A(n). T Alg(T(n,-),A) \simeq A(n) \,.

Notice that this extends to a functor

F T():FinSetTAlg F_T(-) : FinSet \to T Alg

which is the composite

F T():FinSeti T opT opjTAlg F_T(-) : FinSet \stackrel{i_T^{op}}{\to} T^{op} \stackrel{j}{\to} T Alg

of the Yoneda embedding with the opposite of the canonical functor i T:FinSet op𝒮Ti_T : FinSet^{op} \simeq \mathcal{S} \to T from the theory of sets, described above.

More generally, for SSetS \in Set not necessarily finite, let Sub(S)Sub(S) be the poset of finite subsets of SS and their inclusions.

Then F T(S)F_T(S) is the filtered colimit of the representables corresponding to the finite subsets

F T(S)lim nSub(S)T(n,). F_T(S) \simeq {\lim_{\to}}_{{n \in Sub(S)}} T(n,-) \,.

As discussed below, these filtered colimits of TT-algebras are computed objectwise.

Adjunctions of relatively free TT-algebras

The following establishes that more generally any morphism of Lawvere theories leads to an adjunction between their categories of algebras.

Let T 1T_1 and T 2T_2 be Lawvere theories and f:T 1T 2f : T_1 \to T_2 a morphism. Write f *:T 2AlgT 1Algf^* : T_2 Alg \to T_1 Alg for the functor on categories of algebras induced by precomposition with ff.

Lemma

The functor f *f^* has a left adjoint f *:T 1AlgT 2Algf_* : T_1 Alg \to T_2 Alg.

Proof

Here is an elementary proof:

Let F T iU T iF_{T_i} \dashv U_{T_i} be the two free algebra/underlying-set adjunctions. For AA a T 1T_1-algebra there is a T 1T_1-congruence Γ\Gamma such that

AF T 1U T 1(A)/Γ. A \simeq F_{T_1} U_{T_1}(A) / \Gamma \,.

Since for any set SS we have U T 1F T 1(S)U T 2F T 2(S)U_{T_1} F_{T_1}(S) \subset U_{T_2} F_{T_2}(S) it follows that ΓT T 2F T 2U T 1(A)\Gamma \subset T_{T_2} F_{T_2} U_{T_1}(A). For Γ\langle \Gamma \rangle the smallest T 2T_2-congruence containing Γ\Gamma we have that F T 2U T 1(A)/ΓF_{T_2} U_{T_1}(A) / \langle \Gamma \rangle is a T 2T_2-algebra.

This one checks is f *Af_* A.

Here is a more high-powered way to obtain this using the monads K iK_i whose algebras are T iT_i-algebras:

for AA a T 1T_1-algebra let f *A:=K 2 K 1Af_* A := K_2 \circ_{K_1} A the the evident reflexive coequalizer

K 2K 1AK 2AK 2 K 1A K_2 K_1 A \stackrel{\to}{\to} K_2 A \to K_2 \circ_{K_1} A

in T 2AlgT_2 Alg.

Limits and colimits of TT-algebras

Proposition

For TT a Lawvere theory, the category TAlgT Alg has all small limits and colimits.

The limits and the filtered colimits in TAlgT Alg are computed pointwise.

The category of algebras TAlgT Alg has a zero object if and only if TT has a single nullary operation (Proposition 3.3 of Wraith).

An open problem

A famous result by G. Higman in group theory says that a finitely generated group can be embedded in a finitely presented group precisely if it has a presentation whose defining relations are a recursively enumerable set of words. Clearly, this question can be asked for every similar algebraic theory and it has been in fact conjectured by the group theorist W. Boone that the same result holds more generally for every single-sorted algebraic theory. While in fact the conjecture is not true for all single-sorted algebraic theories (see Boone conjecture for further details), as was known by Soviet mathematicians, the general question “In which algebraic categories does (an analogue of) Higman’s embedding theorem hold?” is still interesting. In fact, it has been urged by F. W. Lawvere on several occasions that this Boone conjecture should be settled by the category theory community.

References

The origin of the categorical formulation of algebraic theories as Lawvere theories is in

The concept was then streamlined in

  • Samuel Eilenberg, J. B. Wright, Automata in General Algebras , Information and Control 11 (1967) pp.452-470.

Also still worthwhile reading are the following early papers:

  • Gavin Wraith, Algebraic Theories , Aarhus Lecture Notes Series no.22 (1969). (pdf, 3,7MB)

  • Gavin Wraith, Algebras over Theories , Colloquium Mathematicum XXIII no.2 (1971) pp.181-190. (link)

An early textbook treatment was in

  • Bodo Pareigis, Categories and Functors , New York: Academic Press 1970. (chap. 3; link)

Modern textbook treatments are

  • Francis Borceux, Handbook of categorical algebra 2 – Categories and structures , Encyclopedia of Mathematics and its Applications, Cambridge UP 1994. (chap. 3)

  • M. C. Pedicchio, F. Rovatti, Algebraic Categories , pp.269-310 in Pedicchio, Tholen (eds.), Categorical Foundations , Encyclopedia of Mathematics and its Applications 97, Cambridge UP 2004.

A recent monograph is

The concept of an internal algebraic theory in topos theory is dicussed in

  • Peter Johnstone, Gavin Wraith, Algebraic theories in toposes , pp.141-242 in LNM 661 Springer Heidelberg 1978.

  • Peter Johnstone, Topos Theory , Academic Press New York 1977. (Dover reprint 2014; sec. 6.4, pp.190-198)

Comparison with the notion of monads:

An elementary proof of the equivalence between infinitary Lawvere theories and monads on the category of sets is given in Appendix A of

Distributive laws for algebraic theories are discussed in

Voevodsky proves an equivalence between Lawvere theories and l-bijective C-systems here:

Other references are

  • M. Jibladze, T. Pirashvili, Cohomology of Algebraic Theories , J. Algebra 137 no.2 (1991) pp.253–296.

  • Steve Lack, Jiri Rosicky, Notions of Lawvere theory , arXiv:0810.2578. (abstract)

  • Enrico Vitale, Localization of Algebraic Categories , JPAA 108 (1996) pp.315-320.

  • Enrico Vitale, Localization of Algebraic Categories 2 , JPAA 133 (1998) pp.317-326.

Lawvere theories, and finitary monads, are identified with certain enriched categories and the passage from one to the other with a cocompletion, in

Some properties of Lawvere theories:

  • V. Trnková, Representability and local representability of algebraic theories, algebra universalis 39.3 (1998): 121-144.

A short introductory/overview note:

  • Andreas Nuyts, Understanding Universal Algebra Using Kleisli-Eilenberg-Moore-Lawvere Diagrams, note

Last revised on July 20, 2024 at 09:53:51. See the history of this page for a list of all contributions to it.